An ongoing problem in the design of large systems is verifying that the system will behave in the manner intended by its designers. One approach has been to simply try out the system, either by building and testing the system itself or by building and testing a model of the system. Since there is no guarantee that an untested system will work as expected, building the system itself can be an expensive proposition. Thus, those skilled in the art have migrated toward building and testing a model of the system, or system model, through software.
A system model can be said to be a computer program or block of code that, when executed, simulates the intended properties, or functions, of the system. Basically, the system model is designed to accept inputs, perform functions and generate outputs in the same manner as would the actual system. To do this, the system model uses variables, called system-model variables, that are programmed within the code to take on certain values depending on the values of the inputs to the system model. That is, as different values are fed to the system-model inputs, the system-model variables are assigned different values that indicate how the system model functions or behaves in response to the inputs. Thus, by controlling the value of the inputs to the system model and monitoring the values of the system-model variables, a system designer can test or observe the behavior of the system model in response to different sets of inputs, and determine whether the system model exhibits, or performs, the intended properties of the system.
One method of testing a system model in such a manner is called formal verification. In formal verification, a verification tool is used to convert the system model into a finite state machine. A finite state machine is a set of states and state transitions which mimic the operation of the system model in response to given sets of inputs, or input vectors. The term "set of inputs" as used herein refers to the values input to each system-model input at any given time, and the term "input vectors" as used herein refers to the sets of inputs successively fed to the system model inputs over a period of time.
In general, each state of a finite state machine represents a specific assignment of values to a set of system-model variables, and thus represents a specific behavior of the system model. Each state transition defines the values that a set of system-model inputs and/or system-model variables must take on for the state machine to transition from one state to another state. The state machine thereby provides a roadmap of how a system model will behave, i.e. the states the system model will enter, in response to the values input to the system-model inputs. As a result, once the verification tool converts the system model into such a finite state machine, the tool can use the state machine or roadmap to test the behavior of the system model.
To illustrate, conventional verification tools, such as the explicit-state enumeration-based verification tool described by R. P. Kurshan in Computer Aided Verification of Coordinating Processes, Princeton University Press 1994, are designed to test the behavior of the system model by performing a so-called search of the system-model state space (i.e. the set of states and state transitions that represent the behavior of the system model). Conventionally, a search is performed by inputting to the system model a "complete set of inputs" at each state of the system model, and monitoring the behavior of the system model in response thereto. The term "complete set of inputs" as used herein refers to every possible set of values that the system-model inputs can possibly assume when the system model is in operation, in every possible sequence. Such a complete set of inputs is an input vector.
The more complex a system model becomes (i.e. the greater the number of system model inputs, the wider the range of assumable values for each input, and/or the greater the number of states or system model variables), the greater the amount of computational resources and/or time necessary to complete a search of the system-model state space. In fact, it has been found that performing a search of a sufficiently complex model with a conventional verification tool can cause the verification tool to run out of computational resources (e.g. no more RAM available to the search engine). When this happens, the verification tool may "lock-up", or stop the search, without providing the tester with data as to whether the system model had behaved as expected for any part of the search performed before the "lock-up." As a result, when performing a conventional search on such complex system models, the tester may be left with no way of determining whether the system model has a design error.
One solution to this problem is to reduce the size of the system model and run a search on the reduced model. That is, a tester or programmer experienced in the details of the system model, including how the system-model inputs and system-model variables affect the behavior of the system model, may eliminate portions of the system model, including lines of code and/or system-model inputs and variables, that appear to have no effect on a limited set of system behaviors or functions which the programmer decides are not critical to check. To do this, the programmer must take care to insure that the system model is not reduced such that the reduced model fails to retain those portions of the code that define the behaviors the programmer intends to test. This may require, however, substantial time, effort and experience on the part of the programmer.
Thus, from all of the above, it can be appreciated that when using conventional formal verification tools to identify errors in a system model, the available computational resources may be fully exhausted before completion of the test, and/or the tester may be required to posses a high degree of skill for predetermining how to reduce the size of the system model without eliminating the so-called critical parts.